
\chapter{Native Interface} \label{native interface}

\todo{This chapter is not yet complete.}

In this chapter, we describe how \hyperref[nativedat]{native data types} and \hyperref[nativefun]{native functions} work, establish some conventions for the work with mutable data types
and give a receipt for creating correct native function declarations.

\section{Purpose of the Native Interface}

The language constructs introduced so far make it possible to write \emph{pure} functional programs. Pure functional programs consist of pure functions that work on immutable data. For the purpose of this discussion, we define these terms as follows: 

\begin{description}
\item[pure function] A function $f$ is pure, if the following holds:
\begin{itemize}
\item $f$ computes the same result when given the same argument values during execution of the program that contains $f$.
\item The result must only depend on the values of the arguments, immutable data and other pure functions. Specifically, it may not depend on mutable state, on time or the current state of the input/output system.
\item Evaluation of $f$ must not cause any side effect that could be observed in the program that evaluates $f$. It must not  change the state of the real world (such as magnetic properties of particles on the surface of a rotating disc).
\end{itemize}
This definition is not as rigid as others that can be found in the literature or in the Internet. For example, we may regard a function \exq{\term{getenv} \sym{::} \term{String} $\rightarrow$ \term{String}} as pure, even if it depends on some hidden data structure that maps string values to other string values (the environment), provided that it is guaranteed that this mapping remains constant during program execution. 

Regarding side effects, we exclude only effects in the real world (input/output, but not physical effects in the CPU or memory chips) and effects that are observable \emph{by the program that caused it}. For example, evaluation of the expression
\exq{ s1 ++ s2 }
where \term{s1} and \term{s2} are string values, will cause creation of a new \java{} \term{String} object and mutation of some memory where the new string's data is stored, this could even trigger a garbage collector run with mutation of huge portions of the program's memory. Yet, all this happens behind the scene and is observable only by \emph{another} program such as a debugger or run time monitor, if at all.

We also do not insist that application of a pure function with the same argument values must return the same value in different executions of the program\footnote{If we did insist on equal return values for application of a pure function with equal arguments \emph{in different executions of a program}, we could not use any functionality provided by the underlying platform, which is in our case \java{} and the \java{} Virtual Machine. For we could not guarantee that certain constants or pure methods we use will be unchanged in the next update or version of that component. 

Alternatively, one could of course define the term \emph{program} in such a way that it encloses a specific version of the \java{} runtime system (and in turn specific versions of the libraries used by \java{}, and the libraries used by those libraries down to the operating system and even the hardware). But then, the term \emph{program} would become almost meaningless.
Suppose, for example, that some chip producer finds a bug in one of the floating point units that he produces, which causes incorrect results to be returned by certain floating point divisions. Suppose further, that the faulty CPU chip is replaced by a fixed one in the computer used by an extremely rigid functional purist, who insists that functions must produce the same value across different program executions. Then, this person must either admit that some function he wrote was not pure (because it suddenly produces different results for the same argument values) or he must regard his program as having changed. He could, for instance, talk about how much more exact results "\emph{this new version of my program}"  produces, despite nobody hasn't changed a single bit on the hard disk!

This argumentation is not invalidated by pointing out that the faulty CPU did not behave according to their specification. It remains the fact that results of computer functions depend on the computing environment they are executed in, no matter if one likes it or not.

It is probably more rational to acknowledge that the idea of a function that \emph{depends on nothing but its arguments} is a nice, but utterly idealistic one that must necessarily abstract away many aspects of reality. In practice, the result of a function $\backslash x \rightarrow x/3145727.0$, when defined in some computer language and executed in some computing environment depends not only on $x$, but also on how the floating point unit works, how exact the divisor can be represented in floating point, in short, it depends on the computing environment where it is run. 

We do not understand the concept of functional purity so narrowly that we require the same result of a pure function in all thinkable computing environments. Rather, we admit realistically that results may be different in different computing environments. The session environment (the mapping of values printed by the command \term{env} in a \textsc{Unix} session; similar features exist in other operating systems) is a part of the computing environment that is constant during program execution (in \java{} programs, that is). Hence, the result of a pure function in a program may depend on environment variables, according to our definition. It may depend on the arguments passed on the command line. Yet, it may not depend on the current directory, for obtaining the name of it or using it presupposes input/output to be performed. It may also not depend on \java{}s system properties, for those can be changed during program execution.}.

\item[immutable values] A value is immutable if there are no means to \emph{observably} change it or any values it contains or references.

This is deliberately vague in view of the difficulties in \java{} when it comes to enforcing immutability. \footnote{It is, for example.possible to break intended immutability with the help of  the reflection API.}
\end{description}

The native interface allows to call \java{} methods and use \java{} data in \frege{} programs.
Because \java{} reference values  may be mutable and \java{} methods may not be pure functions, it provides means to differentiate between pure vs. impure methods and mutable vs. immutable values. Unfortunately, there exists no reliable general way to establish purity of \java{} methods or immutability of \java{} values. Therefore, the \frege{} compiler must rely on the truthfulness of the annotations the programmer supplies.

\hasdiff{The native interface in \frege{} 
corresponds to the \emph{Foreign Function Interface} in Haskell 2010 (\cite[Chapter 8]{h2010}), but differs in the following points:
\begin{itemize}
\item There are no foreign exports, because all items defined in a \frege{} module that are visible
in other \frege{} modules are also visible to any \java{} program anyway.
\item Foreign imports (i.e. native declarations) always refer to items known in the \java{} virtual machine. 
The source language that was used to create those classes, interfaces or methods is immaterial.
\item There are no calling conventions to choose from.
\item Some simple marshaling between \frege{} data and JVM data is supported.
\end{itemize}}


\section{Terminology and Definitions}

Let's recall the general forms of native data and function declarations:
\begin{quote}
\begin{flushleft}
\textbf{data} $T$ $t_1$ $\cdots$ $t_i$ = \textbf{native} $J$\\
\textbf{native} $v$ $j$ :: $t$
\end{flushleft}
\end{quote}

We call $T$ a \emph{native type} and $J$ the \emph{java type} associated with it. 
We also say that the \frege{} type ($T$ $t_1$ $\cdots$ $t_i$) denotes the \java{} type $J$.
In this chapter, we'll use the abbreviations \jt{$T$} for \emph{the \java{} type associated with or denoted by T}
and \ft{$J$}for \emph{the \frege{} type that denotes J}.

If $T$ is associated with one of 
\texttt{byte}, \texttt{boolean}, \texttt{char}, \texttt{short}, \texttt{int}, \texttt{long}, \texttt{float} or \texttt{double}, 
then $T$ denotes a \emph{primitive type}, otherwise it denotes a \emph{reference type}.

We call $v$ a \emph{native value} and $j$ the \emph{java item} associated with it. If $t$ is of the form $t_1 \rightarrow{} \cdots{} \rightarrow{} t_k \rightarrow{}t_R$, where $t_R$ is not itself a function type, we call $v$ a \emph{native function} with \emph{arity} $k$ $(k\ge 1)$ and \emph{return type} $t_R$. The $t_i$ are called \emph{argument types}. For $v$'s that are not native functions, the arity is 0 and the return type is $t$.

$J$ and $j$ are snippets of \java{} code and can be specified as identifiers, qualified identifiers or operator symbols as long as this does not violate the \frege{} lexical syntax. In all other cases the code snippets can be given in the form of string literals. In the following sections, we will frequently use the value of $j$ or just $j$. This is to be understood as the string that is described by the string literal, not the string literal itself.

\section{Mapping between \frege{} and \java{} Types}

Since all \frege{} types must be mapped to \java{} types eventually, 
it is the case that every \frege{} type of kind \sym{*} denotes exactly one \java{} type. 
The converse, however, is not true, since multiple \frege{} 
types may map to one and the same \java{} type\footnote{Implementations are free to erase type arguments, 
so that, for example \term{Maybe String} and \term{Maybe Int} may denote the same \java{} type. 
In fact, since \java{}'s type system is not powerful enough to deal with higher kinded types, 
it is very likely that type arguments will be erased.}
and in addition, \ft{$J$} is only defined for
those \java{} types that are made available to \frege{} with a native data definition.

The \autoref{typemapping} shows a recommended mapping.

\begin{figure}[hbt]
\begin{tabular}{|c|c|p{5cm}|}
\hline \rule[-1ex]{0pt}{1.5ex} Type $T$ & \jt{$T$} & Comment \\ 
\hline \rule[-1ex]{0pt}{1.5ex} $a$ & \texttt{java.lang.Object} & \small nothing is known about values of type $a$\\
\hline \rule[-1ex]{0pt}{1.5ex} $a$ $\rightarrow$ $b$ & \texttt{frege.runtime.Lambda} & \\
\hline \rule[-1ex]{0pt}{1.5ex} \texttt{Bool} & \texttt{boolean} & \\
\hline \rule[-1ex]{0pt}{1.5ex} \texttt{Int} & \texttt{int} & \small and similarly for all other primitive types\\
\hline \rule[-1ex]{0pt}{1.5ex} \texttt{String} & \texttt{java.lang.String} & \\
\hline \rule[-1ex]{0pt}{1.5ex} \texttt{Integer} & \texttt{java.math.BigInteger} & \\
\hline \rule[-1ex]{0pt}{1.5ex} \bracka{}$a$\brackz{} & \texttt{frege.prelude.PreludeBase.TList} & \\
\hline \rule[-1ex]{0pt}{1.5ex} ($a$, $b$) & \texttt{frege.prelude.PreludeBase.TTuple2} & and similarly for tuples with more components\\
\hline \rule[-1ex]{0pt}{1.5ex} \texttt{JArray} $a$ &  \texttt{java.lang.Object}  & generic array \\
\hline \rule[-1ex]{0pt}{1.5ex} \texttt{JArray} $T$ &  \jt{$T$}\texttt{\lbrack{}\rbrack{}}  & array of T \\
\hline \rule[-1ex]{0pt}{1.5ex} enumerations & \texttt{short} & \\
\hline \rule[-1ex]{0pt}{1.5ex} algebraic & $M$.T$T$ & where $T$ is defined in module $M$\\
\hline 
\end{tabular} 
\caption{Recommended type mapping} \label{typemapping}
\end{figure}


\section{Types with Special Meaning}

The following types have a special meaning in the type signatures of native values and functions. 
They are used to require special handling of argument or return values (marshalling).

As far as \frege{} is concerned, the corresponding values have exactly the declared types.
The \java{} type, however, can be different.

\begin{description}
\item[\texttt{()}] The unit type as argument type indicates an empty argument list for the \java{} method that implements the native function. The unit type is only allowed in argument position if the type is of the form $() \rightarrow t_R$. i.e. when the unit value is the only argument\footnote{Note that \emph{instance methods} always have at least one argument, the so-called receiver. Hence the \frege{} type of an instance method may never be $() \rightarrow t_R$}.

The unit type as return type indicates that the native function is implemented by a \java{} method that is declared \texttt{void}. The compiler supplies a wrapper that invokes the method and returns the value ().

\item[\texttt{Maybe} $a$] A \texttt{Maybe} type in argument position indicates that the \java{} method that implements a native function takes \texttt{null} values for the corresponding argument. The generated code will pass \texttt{null} for arguments with value \texttt{Nothing} and $x$ for arguments of the form (\texttt{Just} $x$).

A \texttt{Maybe} type as return type indicates that the implementing method may return \texttt{null} values. The return value \texttt{null} will be mapped to \texttt{Nothing} and any other return value $j$ to (\texttt{Just} $j$).

It therefore holds that \jt{\texttt{Maybe} $a$} in native method's arguments or return values is \jt{$a$}.

\java{} provides classes for boxed primitive values, like for instance \texttt{java.lang.Float}. 
If one needs to use a method that has an argument of a boxed type, 
one can use any \frege{} type that is associated with the corresponding  primitive type (i.e. \texttt{Float}). 
This works because \java{} performs \emph{autoboxing}. 
However, if one ever needs to pass \texttt{null}, the corresponding argument type must be wrapped in \texttt{Maybe} (i.e. \texttt{Maybe Int}). 
For return types, the autoboxing works in a similar way. 
Yet, whenever it is not provably impossible that the method ever returns \texttt{null}, 
one must declare the return type as a \texttt{Maybe} type. 
Failure to do so may cause null pointer exceptions to occur at runtime.

The type wrapped by \texttt{Maybe} must not be any of the special types described here.


\item[\texttt{Either} $x$ $t$] This type is to be used as return type instead of $t$ when the implementing method is declared to throw checked exceptions or if it is known that it throws other exceptions that one needs to catch.

The $x$ must be an \emph{exception descriptor} whose definition follows along with two other concepts we will be using:
\begin{itemize}
\item If \jt{$x$} is some \java{} type that implements \texttt{java.lang.Throwable}, then and only then is $x$ a \emph{throwable type}. \label{throwable}
\item If $x$ is a throwable type, it is a valid \emph{exception descriptor}. \label{descriptor}
\item Let $y$ be an exception descriptor and $t$ a throwable type. 
Then \texttt{Either} $y$ $t$  is a valid exception descriptor.
\item All other types are not exception descriptors.
\item A type of the form \texttt{Either $x$ $t$} 
where $x$ is an exception descriptor and $t$ is not an exception descriptor is called a \emph{catching type}.
\label{catching}
\end{itemize}

The \hyperref[nested-either]{nested \texttt{Either}} syntax comes in quite handy here:

\example{\tt \small
\begin{flushleft}
data BadCharset = pure native \\
\hspace{2cm}java.nio.charset.IllegalCharsetNameException\\

data UnsupportedCharset = pure native \\
\hspace{2cm}java.nio.charset.UnsupportedCharsetException\\

data CharSet = pure native java.nio.charset.Charset where\\
\hspace{1cm}pure native csForName java.nio.charset.Charset.forName \\
\hspace{2cm}:: String -> (BadCharset|UnsupportedCharset|CharSet)
\end{flushleft}
}

Code generation  will create a wrapper method containing a \texttt{try} statement with \texttt{catch} clauses
that catch the exceptions declared in $x$ in left to right order\footnote{
The order is the same, regardless of notation of the type as \texttt{(Either (Either E1 E2) R)} or \texttt{(E1|E2|R)}.
It could appear to be different only if one used type aliases like \texttt{type Rehtie a b = Either b a}, 
however, it is the order in the expanded form that counts.}.

Note that the \java{} language enforces certain rules for exception handling (see \cite[§11]{langspec3}). The following points should be observed to avoid \java{} compiler errors:

\begin{itemize}
\item The catching type must list all checked exceptions that the method may throw.
\item The catching type must not list any exception the method may not throw.
\item In the catching type, more specific exceptions (in terms of the \java{} exception class hierarchy, see \cite[§11.5]{langspec3})
must occur further left than less specific ones. 
\end{itemize}

If the wrapper indeed catches one of the interesting exceptions, it constructs an appropriate \texttt{Left} value.
Otherwise, if a value $v$ is returned from the native method, the wrapper returns (\texttt{Right} $v_m$), 
where $v_m$ is the value after marshalling of $v$, 
which takes place in cases where $t$ is one of the types with special meaning as explained before.

A \hyperref[catching]{catching type} is not valid as argument type for a native function. 

$t$ may not be another catching type nor a \texttt{ST} or \texttt{IO} type.

\item[\texttt{ST} $s$ $t$] This type must be used when the implementing method uses or produces mutable data. 
\texttt{ST} must be the outermost type constructor in the result type. 

The compiler creates an appropriate wrapper function that constructs a \texttt{ST}  action, which, when executed, runs the native method and returns its value in the \texttt{ST} monad. Native functions declared this way can also be used in the \texttt{IO} monad.

\item[\texttt{IO} $t$] This type must be used when the implementing method has any \hyperref[pure]{side effects}. \texttt{IO} must be the outermost type constructor in the result type. 
The compiler creates an appropriate wrapper function that constructs an \texttt{IO}  action, which, when executed, runs the native method and returns its value in the \texttt{IO} monad.

\end{description}

For an overview of possible return values of native functions see \autoref{nativertys}.

%\begin{onecolumn}
\begin{figure*}[bth]
\begin{center}
\begin{tabular}{llp{0.3\textwidth}}
\textbf{\small declared return type} & \textbf{\small expected java signature} & \textbf{\small example java code or comment} \\
& & \\
\texttt{\small ()} & \texttt{\small void meth(...)} & \texttt{\small System.exit()}\footnotemark[1] \\
\texttt{\small (Ex|())} & \texttt{\small void meth(...) throws \jt{Ex}\footnotemark[2]} & \texttt{\small System.arraycopy(...)}\footnotemark[1] \\
\texttt{\small IO ()} & \texttt{\small void meth(...)} & \texttt{\small System.gc()} \\
\texttt{\small IO (Ex|())} & \texttt{\small void meth(...) throws\footnotemark[2] ...} & \texttt{\small (Thread)t.start()}\\
\texttt{\small Int} & \texttt{\small int meth(...)} & \texttt{\small (String)s.length()} \\
\texttt{\small String} & \texttt{\small java.lang.String meth(...)} & \texttt{\small (String)s.concat(...)} \\
{\small $a$}\footnotemark[3] & {\small \jt{$a$}} \texttt{\small meth(...)} & {\small general rule, note that previous 2 lines are no exceptions} \\
\texttt{\small Maybe Int}\footnotemark[4]& \texttt{\small java.lang.Integer meth(...)} & \texttt{\small Integer.getInteger(...)} \\
{\small \texttt{Maybe} $a$}\footnotemark[3] & {\small \jt{$a$}} \texttt{\small meth(...)} & {\small general rule for any $a$ that is not a primitive type} \\
{\small (\texttt{Ex|}$a$)}\footnotemark[5] & {\small same as for $a$ + \texttt{throws\footnotemark[2] ...}} & \texttt{\small Float.parseFloat(...)}\footnotemark[7] \\
{\small \texttt{IO} $a$}\footnotemark[6] & {\small same as for $a$} & \texttt{\small System.nanoTime()}\footnotemark[8]\\
{\small \bracka{}$a$\brackz{}}\footnotemark[3] & {\small \jt{$a$}\bracka{}\brackz{} meth(...)} & \texttt{\small (String)s.split(...)\footnotemark[9]}\\
{\small \bracka{}$a$\brackz{}}\footnotemark[3] & \texttt{\small Iterator<\jt{$a$}> meth(...)} & \texttt{\small List<String>l.iterator(...)\footnotemark[9]}\\
\end{tabular}
\end{center}
\caption{Well formed native return types} \label{nativertys}

\begin{footnotesize}
\vspace{3mm}
\footnoterule
\footnotemark[1]{However, the compiler can not be fooled into thinking that such a method is actually pure. Therefore, despite the return type is well-formed, it's still invalid. If you need a function that maps any argument to \texttt{()}, consider \texttt{const ()}}

\footnotemark[2]{If the \java{} method actually declares checked exceptions, the return type must be a catching type or the \texttt{throws} clause on the native declaration must be used.}

\footnotemark[3]{where $a$ is no type with special meaning}

\footnotemark[4]{This works in a similar way for all other primitive types. The code generated by the compiler expects a value of the corresponding boxed type or \texttt{null}. Note that, because \java{} does autoboxing of primitive values, methods that return the corresponding primitive value are also allowed.}

\footnotemark[5]{where $a$ is not another catching type and not an \texttt{IO} type}

\footnotemark[6]{where $a$ is not another \texttt{IO} type}

\footnotemark[7]{in this case, $a$ would be \texttt{Float}}

\footnotemark[8]{in this case, $a$ would be \texttt{Long}}

\footnotemark[9]{in this case, $a$ would be \texttt{String}}
\end{footnotesize}
\end{figure*}


\section{Exception Handling}

There are two mechanisms that deal with exceptions thrown from native functions. 
The first mechanism uses \hyperref[catching]{catching types} 
as described in the previous section. 

The idea behind the catching types is to encode the actual return value and the catched exceptions in a value of type \texttt{Either}.
This makes it in effect impossible to overlook that the function may throw exceptions. 
The user has many choices to get at the actual return value: case expressions, the \texttt{either} function, or higher order functions like \texttt{fmap}. But he cannot pretend that the function just returns a value without taking the possibly of thrown exceptions into account.

This approach is fine in many cases, but may be a bit laborious in others. 
For example, when doing input/output using \java{} APIs, almost every function will potentially throw some incarnation of \texttt{java.io.IOException}. 
It is neither desirable nor even possible to ignore such exceptions, and this could lead to a programming style where every function call is followed by long winded error handling. In the end, even small sequences of I/O actions could result in deeply nested case expressions. Or the code could get extremely fragmented along the lines of:

\example{\tt
\begin{flushleft}
processFile path = do\\
\hspace{0.5cm}openFile path >>= either handleOpenException continueRead\\

continueRead f = do\\
\hspace{0.5cm}readLine f >>= either handleNoLine (processLine f)\\

processLine f ln = do\\
\hspace{0.5cm}result1 <- do something with the line\\
\hspace{0.5cm}readLine f >>= either handleNoOtherLine (processRest f result1)\\

processRest f res1 ln2 = do ....\\

handleOpenException ex = do ...\\

handleNoLine ex = do ....\\

handleNoOtherLine ex = do ....\\
\end{flushleft}
}

Should a function throw different exceptions that require separate handling, it will get even more complex.

Therefore, there is another approach, that allows to catch and handle exceptions explicitly 
in the \texttt{ST} or \texttt{IO} monads\footnote{The details of how to use the key functions \texttt{catch} and \texttt{finally} and how to write exception handlers can be found in the API documentation.}.

The explicit approach rests on the idea that the return types of native functions are left as they are, 
except for the \texttt{ST} or \texttt{IO} wrapper.
This requires, however, that checked exceptions, 
which are part of \java{} method signatures must be eliminated,
since \frege{} function types carry no information about them.

Put differently, a \java{} method that invokes a method whose signature states that checked exceptions may be thrown must do so either inside of a throw/catch statement where the checked exception is catched, or the calling method must itself state that it throws the exception.

Neither are there statements in \frege{}, let alone try/catch statements, 
nor are exceptions part of the contract of \frege{} functions. 
Hence, the only possibility is to catch the exceptions where they arise, 
wrap them in unchecked exceptions and re-throw the latter ones, 
which can be done without changing the method's signature.

To achieve this, the following form of a native function declaration must be used:

\begin{flushleft}
\textbf{native} $v$ $j$:: $t$ \textbf{throws} $x_1$, $\cdots$, $x_k$
\end{flushleft}

Here, $t$ is the function type whose return type must be a \texttt{ST} or \texttt{IO} type, and the $x_i$ ($i \ge 1$) are \hyperref[throwable]{throwable types} that denote \java{} exceptions to re-throw. The generated wrapper will create a try/catch statement that catches, wraps and re-throws all exceptions denoted by the $x_i$.

\subsection*{Declaration of Throwable Types}

\hyperref[throwable]{Throwable types}  are to be declared like in the following example:

\example{\tt
\begin{flushleft}
data IOException = pure native java.io.IOException\\
derive Exceptional IOException
\end{flushleft}
}

The declarations shown are imported from package \texttt{frege.java.IO} and are thus available in every \frege{} program. However, not all exceptions from the JRE may be predeclared, and exceptions from 3rd party libraries will certainly not be predeclared.

The convention is to view throwable types as abstract, immutable tokens, hence the \texttt{pure native} declaration. In addition, if one wants to catch exceptions explicitly with the \texttt{catch} function, one needs to make the throwable type an instance of \texttt{Exceptional}. This is because the type of \texttt{catch} is

\begin{code}
catch :: Exceptional e => IO a -> (e -> IO a) -> IO a
\end{code}

where the second argument is the exception handler. Hence, to use an exception handler that handles exception $e$ with \texttt{catch}, $e$ must be an instance of type class \texttt{Exceptional}.

\subsection*{Rules for Native Functions that Throw Exceptions}

\begin{itemize}
\item The set of checked exceptions declared in the signature of the \java{} method must be a subset of the throwable types in the native declaration, otherwise the generated \java{} code will not compile. Put differently, 
all possible checked exceptions must be considered in one way or the other by the \frege{} declaration.
\item Catching types and the \texttt{throws} clause can be combined, as long as the set of exceptions handled with catching types is disjunct from the set of exceptions named in the \term{throws} clause. The exceptions occurring in the catching type will never be thrown, but wrapped in the \texttt{Either} value.
\item Catching types as well as throws clauses can contain additional unchecked exceptions.
\item Native functions with \texttt{throws} clauses allow one to deliberately ignore exceptions, even checked ones.
Needless to say, except for toy programs, this is not acceptable, as 
any unhandled re-thrown exception will terminate the thread where it was raised.
\end{itemize}

\section{Mutable and immutable \java{} data} \label{mutable-immutable-data}

Most \java{} objects are potentially mutable. 
However, from the \frege{} point of view the question is whether objects of a certain class can be mutated with the operations that are available. If one restricts oneself to non-mutating native functions, 
a \java{} class can be considered immutable for the purpose at hand. 

An example for such a border case is \texttt{java.math.BigInteger}, which is technically not immutable at all, 
yet offers a quite functional interface. 
With the understanding that malicious \java{} code could manipulate big integer values, 
this class is regarded immutable in \frege{}, and serves as implementation for type \texttt{Integer}. Of course, none of the
operations provided for \texttt{Integer} does manipulate the underlying \java{} object in any observable way.

It follows a discussion of the three main categories of native data that are recognized by the \frege{} system.

\subsection{Immutable Only Data}

Native data types declared with the \texttt{pure native} keywords are regarded as truly immutable. For such data, it doesn't matter, if a reference to one and the same object is shared between \java{} and \frege{} code or even between different threads.

There are no restrictions on the use of values of such types.

\note{The behavior and result of programs that incorrectly declare mutable \java{} types as immutable is undefined. It is a programming error the \frege{} compiler unfortunately cannot detect.}

\subsection{Mutable/Immutable Data and the ST Monad}

The normal case are native data that are (by the very nature of the \java{} language) mutable, but can nevertheless be used to model overall pure functions. The corresponding \term{data} declaration for such types uses the keyword \term{native} without additional keywords.

A characteristic property of \java{} classes that belong to this category is that they offer a mix of pure and impure methods.

Common examples are arrays, collections and types like \texttt{java.lang.StringBuilder}, a mechanism for efficient construction of character strings.

The problem in \frege{} is to distinguish between values (i.e. \java{} objects) 
whose references could be aliased and held in parts of the code that is not written in \frege{} (like library code) 
or even in different threads and, on the other side, 
"safe" values that are only known in the \frege{} realm.

The solution is to have a different compile time type for values that are actually mutable and values that are safe. Specifically, we will wrap mutable values of type $M$ in the following type:

\begin{code}
abstract data Mutable s m = Mutable m
\end{code}

Observe that \texttt{Mutable} itself is declared \term{abstract}, which makes it impossible to actually create or deconstruct such a value in \frege{} code, as the value constructor is inaccessible.

Furthermore, the following rules will be enforced for every native type $M$ that is not \term{pure}:

\begin{enumerate}
\item The only way $M$ can appear in the return type of a native function is \term{Mutable} $s$ $M$
\item A pure native function may not return \term{Mutable} $s$ $M$
\item The only way $M$ can appear in the argument type of an impure native function is \term{Mutable} $s$ $M$
\item The phantom types of type constructors \term{ST} and \term{Mutable} must all be the same in the type of a native method. The phantom type is either a type variable or the constant \term{RealWorld}.
\item A pure function must not normally have arguments of type \term{Mutable} $s$ $M$.
\item A type \term{Mutable} $s$ $a$ where $a$ is not a native type or was declared \term{pure native} or \term{mutable native} (see \autoref{mutableonly}) is illegal in the type of native functions.
\end{enumerate}

Rule 1, 2 and 4 make sure that $M$ values can be created only in the \term{ST} or \term{IO} monad, and that their type appears to be \term{Mutable} $s$ $m$, where $s$ is the appropriate phantom type. 
This means also that such values cannot escape from the corresponding monad. 
For the \term{IO} monad, this is guaranteed because nothing can escape it. 
For the \term{ST} monad, the phantom type prevents execution for any \term{ST} action that has a type like

\begin{code}
ST s (Mutable s M)
\end{code}

from pure code (yet, there is nothing wrong \emph{per se} with such a ST action: it could be used in another ST/IO action, for example).

The motivation for rule 5 is the following: From what has been said in the paragraphs above it should be clear that mutable values can only appear in the \term{ST} monad. If we allowed passing mutable data to pure functions (in a let clause, say), their result would depend on whether the monadic code around it actually mutates the value or not. Consider the following slightly contrived example:

\example{\tt
\begin{flushleft}
data Foo = native some.Foo where\\
\hspace{0.5cm}native new :: () -> ST s (Mutable s Foo)\\
\hspace{0.5cm}native setBar :: Mutable s Foo -> Int -> ST s ()\\
\hspace{0.5cm}pure native getBar :: Mutable s Foo -> Int    -- WRONG!!!\\

bad :: ST s Int\\
bad = do\\
\hspace{0.5cm}foo <- Foo.new ()  -- create a value\\
\hspace{0.5cm}foo.setBar 42       -- set the property\\
\hspace{0.5cm}let r = foo.getBar  -- seemingly pure getter\\
\hspace{0.5cm}foo.setBar 43       -- reset the property again\\
\hspace{0.5cm}return r\\
\end{flushleft}
}

There is no way to tell what the value of \term{(ST.run bad)} should be. 
The \term{let}, judging by its data dependencies,  could get floated left, so that its code in the compiled output appears before the first \texttt{setBar}. 
Or the compiler could in-line the definition of \texttt{r} in the argument of \term{return}. 
Or it could leave it as is. 
In any case, there is no need to evaluate \term{foo.getBar} right away. 
The only thing that can be said is that the result, should it be evaluated at all, would depend on the \emph{then} current state of the object denoted by \term{foo}.

The crucial point here is the declaration of the getter method that wants to make us believe that a getter method applied to a mutable object could be pure. In the general case, this is not so. Hence rule 5, which forbids it.

There are, however, cases where a mutable object does have invariant properties. An easy example is getting the length of an array.

\subsubsection{Making Safe Copies of Mutable Values}

Often, mutable values are used only temporary, as is frequently the case with string buffers. 
In other cases, it are precisely the methods that are pure on the condition that the (technically) mutable value actually is not mutated any more, that interest us.
In the case of arrays, for example, it is common to initialize them (from a list, say), and then enjoy the fast random read-only access in a pure computation.

The rules established above make sure that mutable/immutable values are properly treated. But they do too much insofar as they do not even allow escape of a safe copy of a mutable value yet.

For this purpose, the \term{Mutable} type has the following two functions:

\begin{code}
freeze :: Freezable m => Mutable s m -> ST s m
thaw   :: Freezable m => m -> ST s (Mutable s m)
\end{code}

that allow for controlled construction of safe $M$-values from mutable ones and vice versa. $m$ must have an instance for type class \texttt{Freezable}, whose subclasses \texttt{Cloneable} and \texttt{Serializable} are appropriate for \java{} types that implement the \java{} interfaces with the same names. For instance, making a type $T$, that is associated with a \java{} type that implements \texttt{java.lang.Cloneable}, an instance of \term{Cloneable} (the type class)  is as easy as stating:

\begin{code}
instance Cloneable T
\end{code}

After having properly\footnote{
Unfortunately, however, properly freezing is not easy in the general case. Most often, merely cloning is not enough. Actually implementing \term{freeze} (and the counterpart \term{thaw}) requires great care.}
frozen an object, there should be only one reference through which the copy could be mutated. But because we get this reference as $M$ instead of \term{Mutable} $s$ $M$, we cannot pass it anymore to impure methods due to rule 3. Should one ever need to do this, the frozen value must be thawed first using \term{Mutable.thaw}, which is supposed to make another copy that can be mutated without affecting the still existing frozen value.

\subsubsection{Cheating with Rule 5}

As said before, there are often invariants (like array length) on mutable data that can be expressed as pure native functions, but rule 5 forbids it. Because the whole apparatus described here is to help get things right, not to prevent people that know what they are doing from doing it, there is the following additional function for \term{Mutable}s:

\begin{code}
readonly :: (m -> b) -> (Mutable s m) -> ST s b
\end{code}

This way, we can "lift" pure native functions to work on mutable values. The understanding should be that the result must not depend on the mutable state of the object.

Note that \term{(readonly} \term{id)}  can be used to coerce a mutable value to an immutable one. This is justified in cases where the value was created locally, and one knows that no aliases exist, and the value is henceforth to be regarded as immutable without actually copying something.

\subsection{Mutable Only Data} \label{mutableonly}

A native type $M$ whose values would, by the rules above, appear \emph{everywhere} with type \term{Mutable RealWorld} $M$, is called a \emph{mutable only} type. It can be declared like

\begin{code}
data M = mutable native ...
\end{code}

and can appear in type signatures as just $M$. The compiler will then apply the rules above \emph{as if} the type was \term{Mutable RealWorld} $M$ , with the following consequences:

\begin{itemize}
\item A value of type $M$ can only be created in native functions whose return type is \term{IO} $M$ (due to rules 2 and 4).
\item If $M$ occurs as argument of a native function, that function must have type \term{IO} $a$ for some type $a$ (due to rule 3).
\item \term{Mutable.freeze} is not applicable to $M$. The type checker expects a \term{Mutable} $s$ $m$, but the \emph{as if} above concerns only sanity checks for types of native functions, the normal typing rules will never actually unify \term{Mutable} $s$ $m$ with $M$.
\item It would be possible to \term{Mutable.thaw} a value of type $M$, yet no native function type can contain the type \term{Mutable} $s$ $M$ by rule 6, and hence nothing could be done with the supposedly safe copy (except \term{Mutable.freeze} it again).
\end{itemize}

\section{Pure \java{} methods} \label{pure}

A \emph{pure} \java{} method is a pure function, i.e. it has the following properties:
\begin{itemize}
\item Its return value depends only on its arguments, on constant data and on nothing else.
\item It has no side effects.
\end{itemize}

Dually, a function is not pure if at least one of the following holds:
\begin{enumerate}
\item The method performs any input or output operations.
\item The method changes data that is either visible outside of the method or influences the outcome of subsequent invocations of any other method.
\item It matters, when or how often a method is invoked.
\item It can return different values on different invocations with identical arguments. 
This can be the case when the result of the function depends on mutable state.
\end{enumerate}

In \java{}, like in most imperative languages, the use of impure functions is widespread.
Examples for methods that are impure
\begin{enumerate}
\item creation or removal of files, open a file, read from or write to a file
\item any so called \emph{setter}-method, that changes state of an object. Also, random number generators that employ a hidden \emph {seed}.
\item methods that depend on the time of day
\item methods that depend on default locale settings like number or date formatting that could be changed during the runtime of a program, methods that read so called system properties, registry settings or configuration files.
\end{enumerate}

Nevertheless, \java{} provides many methods and operations that are pure. Most methods of {\tt java.lang.String} are, as well as the methods of \texttt{java.util.BigInteger} and the operations on primitive data types. Many object constructors and getter methods are also pure when they create or 
operate on immutable values.

A pure \java{} method must be declared as such by starting the native declaration with the \term{pure} keyword. It cannot have a return type \term{ST} $s$ $a$ or \term{IO} $a$.

\section{Deriving a \frege{} \texttt{native} declaration from a \java{} method signature}

For every \java{} method signature

\begin{quote}
\begin{flushleft}
$t$ $name$($t_1$ $a1$, $t_2$ $a2$, $\cdots$, $t_n$ $ai$) throws $e_1$, $e_2$ $\cdots$ $e_k$
\end{flushleft}
\end{quote}

where $t$ is the return type, $n$ is the fixed number of arguments
\footnote{Argument lists with a variable number of arguments are not supported.},
$t_1$, $t_1$, $\cdots$, $t_n$  are the types of the arguments, 
$k$ is the number of exceptions thrown and the $e_i$ are the respective exceptions,
the \frege{} type must be

\begin{quote}
\begin{flushleft}
() $ \rightarrow{}$ $f_r$  when $n$ is 0\\
$f_1  \rightarrow{} f_2  \rightarrow{}\cdots \rightarrow{}  f_n  \rightarrow{} f_r$  when $n>0$ and for all $i$ \jt{$f_i$} is $t_i$\\
\end{flushleft}
\end{quote}

\paragraph{Finding the return type}

If $t$ is \term{void}, the principal return type is \texttt{()}. 
In all other cases, it is the \frege{} type that is associated with $t$.

\todo{continue me}

\section{\java{} Constructs Supported by Native Declarations}

Depending on the type and the form of the \java{} item, different \java{} constructs are supported. Except for static field access expressions, native declarations introduce a \frege{} item with a function type. The only special things about such native functions are
\begin{enumerate}
\item that the compiler assumes that they are \emph{strict} in all arguments\footnote{A function is said to be strict in an argument if it with necessity evaluates to undefined if the undefined value is passed for that argument.}
so that lazy values are never passed to native functions
\item that their type must not have type class constraints.
\end{enumerate}
In all other respects, native functions are indistinguishable from all other functions with the same type.

\subsection{Static Field Access Expression}

Native values with arity 0 can be used to access static fields of a \java{} class. 
The corresponding \frege{} value is computed once upon beginning of the program.

\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native} $v$ $j$ :: $t$\\
\end{flushleft}
\par where $t$ is not a function type. Then the expression $v$ will be compiled to the following \java{} code: $j$
}

\example{
Consider the following definition
\begin{flushleft}
\textbf{native} pi java.lang.Math.PI :: Double\\
\end{flushleft}
Then \jex{pi} will be
\begin{flushleft}
java.lang.Math.PI\\
\end{flushleft}
}

The java item should be given as a fully qualified name.


\subsection{Instance Field Access Expression}

Public instance fields can be accessed with an instance field access expression.

\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native}  $v$  \term{".}$j$\term{"} :: $t_o$ $\rightarrow$ $t_r$\\
\end{flushleft}
\par where neither $t_o$ nor $t_r$ are function types, $t_o$ is associated with a \java{} reference type and $j$ is an identifier that is valid in \java{}. Then the application $v$ $x$ will be compiled to a field access expression on the \java{} object that is denoted by expression $x$.
}


\subsection{Method Invocation Expression}

\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native} $v$ $j$ :: $t$\\
\end{flushleft}
\par where $t$ is a function type with arity $k$. 

An application of $k$ arguments to $v$ will be compiled to a method invocation, where special types are marshalled as documented before.
}

If $j$ is a simple name, the type of the first argument must be a native reference type, and an instance method invocation with the first argument as receiver is generated.

If $j$ is a qualified name, a static method invocation will be generated.

Like with all \frege{} functions, extra code will be generated to arrange for curried applications. In certain cases, depending on special return types, a wrapper method will be created. 

\subsection{Class Instance Creation Expression}

Class instances (\java{} objects) can be created with class instance creation expressions.

\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native} $v$ \texttt{new} :: $t$\\
\end{flushleft}
\par where $t$ is a function type with arity $k$ whose return type is associated with a \java{} reference type, 
possibly wrapped in a catching type or a \texttt{ST} type, but not in \texttt{Maybe}, as a \java{} constructor cannot return null. Applications of $v$ to $k$ arguments will eventually invoke the appropriate constructor of the \java{} class that is associated with the return type.
}


\subsection{Binary expressions}
\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native} $v$ $j$ :: $t$\\
\end{flushleft}
\par where $t$ is a function type with arity 2 and $j$ is an operator. 

An application of 2 arguments $a$ and $b$ to $v$ will be compiled to a binary expression, where the compiled $a$ stands left of $j$ and the compiled $b$ stands right.
}

The \frege{} compiler cannot check that the operator is valid in \java{} nor that it can be applied to arguments of the given types.

\example{
\begin{flushleft}
\tt pure native ++ + :: String -> String -> String\\
\tt foo = "foo" ++  "bar"\\
\end{flushleft}
defines the \frege{} operator \texttt{++}. The top level binding \texttt{foo} is compiled to:
\begin{flushleft}
\tt public final static java.lang.String foo = "foo" + "bar"
\end{flushleft}
}

\subsection{Unary expressions}
\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native} $v$ $j$ :: $t$\\
\end{flushleft}
\par where $t$ is a function type with arity 1 and $j$ is an operator. 

An application of an arguments $a$ to $v$ will be compiled to an unary expression, where $j$ is applied to the compiled $a$. 
}

The \frege{} compiler cannot check that the operator is valid in \java{} nor that it can be applied to an argument of the given type.

\example{
\begin{flushleft}
\tt pure native not ! :: Bool -> Bool\\
\tt foo x = not x\\
\end{flushleft}
defines the \frege{} function \texttt{not}. The top level binding \texttt{foo} is compiled to:
\begin{flushleft}
\tt public final static boolean foo(boolean arg) \{\\
\hspace{0.5cm}return !(arg);\\
\}\\
\end{flushleft}
}

\subsection{Cast expressions}
\trans{
Let $v$ be declared as
\begin{flushleft}
\textbf{native} $v$ \texttt{"(}$j$\texttt{)"} :: $t$\\
\end{flushleft}
\par where $t$ is a function type with arity 1 and $j$ is a \java{} type. 

This works like an unary operator with the funny name  \texttt{(}$j$\texttt{)}
}

The \frege{} compiler cannot check that the cast is valid in \java{}.

\example{
\begin{flushleft}
\tt pure native long2int "(int)" :: Long -> Int\\
\tt foo x = long2int x\\
\end{flushleft}
defines the \frege{} function \texttt{long2int}. The top level binding \texttt{foo} is compiled to:
\begin{flushleft}
\tt public final static int foo(long arg) \{\\
\hspace{0.5cm}return (int)(arg);\\
\}\\
\end{flushleft}
}
